A:Type, eq:EqDecider(A), f, g:a:A fp Type, a:A. f || g  f  g(a)?Top  g(a)?Top 

latex

Definitions	Type, f(x), Top, t  T, x:A. B(x), b, A, b, , s = t, Prop, x.A(x), x. t(x), a:A fp B(a), x:AB(x), x  dom(f), P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, False, if b t else f fi, f(x)?z, Void, x:A. B(x), EqDecider(T), f || g, f  g
Lemmas	fpf-ap wf, fpf-compatible wf, fpf wf, deq wf, fpf-join-cap-sq, subtype rel self, fpf-cap wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf